Inference at * 2 
Iof proof for Lemma select nth tl:



1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
  n:{0...||v||+1}, i:{0..((||v||+1) - n)}. nth_tl(n;[u / v])[i] = [u / v][(i+n)] 

latex

 by InteriorProof ((((RepD) 
CollapseTHENM (RecCaseSplit `nth_tl`))) 
CollapseTHENA (
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
CollapseTHENA () inil_term))) 

latex

C1: .....truecase..... NILNIL

C1: 6. n : {0...||v||+1}
C1: 7. i : {0..((||v||+1) - n)}
C1: 8. n  0
C1:   [u / v][i] = [u / v][(i+n)]
C2: 

C2: 6. n : {0...||v||+1}
C2: 7. i : {0..((||v||+1) - n)}
C2: 8. 0 < n
C2:   nth_tl(n - 1;v)[i] = [u / v][(i+n)]
C.

Definitions	T, ff, P  Q, P & Q, P  Q, tt, P  Q, tl(l), if b then t else f fi , Y, nth_tl(n;as), x:A. B(x), True, , t  T, Unit, , {i...j},
Lemmas	assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, int iseg wf, length wf1, int seg wf, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf